first-order predicate calculus

First order predicate calculus is a form of logic which includes fixed values such as 'Socrates', or '42', variables that stand for unknown values and predicates, such as 'is_mortal', but makes a strong sepaaration between predicates and variables. This allows reasoning about the values and variables using the predicates, including the classic {[sylogism}}:

is_human(x)=>is_mortal(x) AND is_human(Socrates)=>is_mortal(x) IMPLIES is_mortal(Socrates)

This separation makes it relatively easy to automate reasoning, but means it is not possible to perform higher level statements or reasoning about the predicates themselves such as "is_equal is transitive".